es:ES, i:Id, P:(discrete state@i).
@i stable state.P(state)  
 e@i. P((discrete state after e))  e'e.P((discrete state after e')) 

latex

Definitions	f(a), x(s), x:A. B(x), t  T, x:A  B(x), A c B, left + right, P  Q, x:AB(x), P  Q, P & Q, P  Q, True, T, ES, Id, discrete state@i, (discrete state after e), E, e loc e' , , (e <loc e'), x.A(x), {T}, x. t(x), WellFnd{i}(A;x,y.R(x;y)), loc(e), s = t, @i stable state.P(state)  , Type, e@i. P(e), e'e.P(e'), pred(e), (discrete state when e), P  Q, SQType(T), s ~ t, Atom$n, <a, b>, {x:A| B(x)}
Lemmas	Id sq, dstate-after-pred, es-dstate-when wf, es-pred wf, es-pred-locl, es-stable wf, es-loc wf, es-locl-wellfnd, es-locl wf, es-le wf, es-E wf, es-le-loc, es-dstate-after wf, es-dstate wf, squash wf, true wf, Id wf, event system wf, es-le-iff